<html>
<head>
    <link rel="stylesheet" type="text/css" href="css/tips.css">
</head>
<body>


    <p>For the embedded local terminal, you can define your favorite shell, 
default tab name, and other settings. 
Choose 
<span class="control">File | Settings</span> (on Windows/*nix) or 
<span class="control">Preferences</span> (on MacOS), 
and then open the page <span class="control">Tools | Terminal</span>. </p>

</body>
</html>
